M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). M.ef(k,x,s,v,w)  Prop 

latex

Definitions	MsgA, M.state, M.da(a), M.ef(k,x,s,v,w), M.ds(x), z != f(x)  P(a;z), b, x  dom(f), product-deq(A;B;a;b), Prop, a:A fp B(a), 1of(t), IdDeq, KindDeq, Top, f(x), f(x)?z, 2of(t), State(ds), Knd, x. t(x), P  Q, Id, x:A. B(x), Valtype(da;k), t  T
Lemmas	fpf-cap-void-subtype, fpf-ap wf, Knd wf, ma-state wf, top wf, Kind-deq wf, fpf-cap wf, Id wf, id-deq wf, pi2 wf, pi1 wf, ma-valtype wf, fpf-trivial-subtype-top, product-deq wf, fpf-dom wf, assert wf, msga wf